↳ Prolog
↳ PrologToPiTRSProof
weight_in(.(X, []), X) → weight_out(.(X, []), X)
weight_in(.(N, .(M, XS)), X) → U3(N, M, XS, X, sum_in(.(N, .(M, XS)), .(0, XS), YS))
sum_in([], YS, YS) → sum_out([], YS, YS)
sum_in(.(0, XS), YS, ZS) → U2(XS, YS, ZS, sum_in(XS, YS, ZS))
sum_in(.(s(N), XS), .(M, YS), ZS) → U1(N, XS, M, YS, ZS, sum_in(.(N, XS), .(s(M), YS), ZS))
U1(N, XS, M, YS, ZS, sum_out(.(N, XS), .(s(M), YS), ZS)) → sum_out(.(s(N), XS), .(M, YS), ZS)
U2(XS, YS, ZS, sum_out(XS, YS, ZS)) → sum_out(.(0, XS), YS, ZS)
U3(N, M, XS, X, sum_out(.(N, .(M, XS)), .(0, XS), YS)) → U4(N, M, XS, X, weight_in(YS, X))
U4(N, M, XS, X, weight_out(YS, X)) → weight_out(.(N, .(M, XS)), X)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
weight_in(.(X, []), X) → weight_out(.(X, []), X)
weight_in(.(N, .(M, XS)), X) → U3(N, M, XS, X, sum_in(.(N, .(M, XS)), .(0, XS), YS))
sum_in([], YS, YS) → sum_out([], YS, YS)
sum_in(.(0, XS), YS, ZS) → U2(XS, YS, ZS, sum_in(XS, YS, ZS))
sum_in(.(s(N), XS), .(M, YS), ZS) → U1(N, XS, M, YS, ZS, sum_in(.(N, XS), .(s(M), YS), ZS))
U1(N, XS, M, YS, ZS, sum_out(.(N, XS), .(s(M), YS), ZS)) → sum_out(.(s(N), XS), .(M, YS), ZS)
U2(XS, YS, ZS, sum_out(XS, YS, ZS)) → sum_out(.(0, XS), YS, ZS)
U3(N, M, XS, X, sum_out(.(N, .(M, XS)), .(0, XS), YS)) → U4(N, M, XS, X, weight_in(YS, X))
U4(N, M, XS, X, weight_out(YS, X)) → weight_out(.(N, .(M, XS)), X)
WEIGHT_IN(.(N, .(M, XS)), X) → U31(N, M, XS, X, sum_in(.(N, .(M, XS)), .(0, XS), YS))
WEIGHT_IN(.(N, .(M, XS)), X) → SUM_IN(.(N, .(M, XS)), .(0, XS), YS)
SUM_IN(.(0, XS), YS, ZS) → U21(XS, YS, ZS, sum_in(XS, YS, ZS))
SUM_IN(.(0, XS), YS, ZS) → SUM_IN(XS, YS, ZS)
SUM_IN(.(s(N), XS), .(M, YS), ZS) → U11(N, XS, M, YS, ZS, sum_in(.(N, XS), .(s(M), YS), ZS))
SUM_IN(.(s(N), XS), .(M, YS), ZS) → SUM_IN(.(N, XS), .(s(M), YS), ZS)
U31(N, M, XS, X, sum_out(.(N, .(M, XS)), .(0, XS), YS)) → U41(N, M, XS, X, weight_in(YS, X))
U31(N, M, XS, X, sum_out(.(N, .(M, XS)), .(0, XS), YS)) → WEIGHT_IN(YS, X)
weight_in(.(X, []), X) → weight_out(.(X, []), X)
weight_in(.(N, .(M, XS)), X) → U3(N, M, XS, X, sum_in(.(N, .(M, XS)), .(0, XS), YS))
sum_in([], YS, YS) → sum_out([], YS, YS)
sum_in(.(0, XS), YS, ZS) → U2(XS, YS, ZS, sum_in(XS, YS, ZS))
sum_in(.(s(N), XS), .(M, YS), ZS) → U1(N, XS, M, YS, ZS, sum_in(.(N, XS), .(s(M), YS), ZS))
U1(N, XS, M, YS, ZS, sum_out(.(N, XS), .(s(M), YS), ZS)) → sum_out(.(s(N), XS), .(M, YS), ZS)
U2(XS, YS, ZS, sum_out(XS, YS, ZS)) → sum_out(.(0, XS), YS, ZS)
U3(N, M, XS, X, sum_out(.(N, .(M, XS)), .(0, XS), YS)) → U4(N, M, XS, X, weight_in(YS, X))
U4(N, M, XS, X, weight_out(YS, X)) → weight_out(.(N, .(M, XS)), X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
WEIGHT_IN(.(N, .(M, XS)), X) → U31(N, M, XS, X, sum_in(.(N, .(M, XS)), .(0, XS), YS))
WEIGHT_IN(.(N, .(M, XS)), X) → SUM_IN(.(N, .(M, XS)), .(0, XS), YS)
SUM_IN(.(0, XS), YS, ZS) → U21(XS, YS, ZS, sum_in(XS, YS, ZS))
SUM_IN(.(0, XS), YS, ZS) → SUM_IN(XS, YS, ZS)
SUM_IN(.(s(N), XS), .(M, YS), ZS) → U11(N, XS, M, YS, ZS, sum_in(.(N, XS), .(s(M), YS), ZS))
SUM_IN(.(s(N), XS), .(M, YS), ZS) → SUM_IN(.(N, XS), .(s(M), YS), ZS)
U31(N, M, XS, X, sum_out(.(N, .(M, XS)), .(0, XS), YS)) → U41(N, M, XS, X, weight_in(YS, X))
U31(N, M, XS, X, sum_out(.(N, .(M, XS)), .(0, XS), YS)) → WEIGHT_IN(YS, X)
weight_in(.(X, []), X) → weight_out(.(X, []), X)
weight_in(.(N, .(M, XS)), X) → U3(N, M, XS, X, sum_in(.(N, .(M, XS)), .(0, XS), YS))
sum_in([], YS, YS) → sum_out([], YS, YS)
sum_in(.(0, XS), YS, ZS) → U2(XS, YS, ZS, sum_in(XS, YS, ZS))
sum_in(.(s(N), XS), .(M, YS), ZS) → U1(N, XS, M, YS, ZS, sum_in(.(N, XS), .(s(M), YS), ZS))
U1(N, XS, M, YS, ZS, sum_out(.(N, XS), .(s(M), YS), ZS)) → sum_out(.(s(N), XS), .(M, YS), ZS)
U2(XS, YS, ZS, sum_out(XS, YS, ZS)) → sum_out(.(0, XS), YS, ZS)
U3(N, M, XS, X, sum_out(.(N, .(M, XS)), .(0, XS), YS)) → U4(N, M, XS, X, weight_in(YS, X))
U4(N, M, XS, X, weight_out(YS, X)) → weight_out(.(N, .(M, XS)), X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
SUM_IN(.(0, XS), YS, ZS) → SUM_IN(XS, YS, ZS)
SUM_IN(.(s(N), XS), .(M, YS), ZS) → SUM_IN(.(N, XS), .(s(M), YS), ZS)
weight_in(.(X, []), X) → weight_out(.(X, []), X)
weight_in(.(N, .(M, XS)), X) → U3(N, M, XS, X, sum_in(.(N, .(M, XS)), .(0, XS), YS))
sum_in([], YS, YS) → sum_out([], YS, YS)
sum_in(.(0, XS), YS, ZS) → U2(XS, YS, ZS, sum_in(XS, YS, ZS))
sum_in(.(s(N), XS), .(M, YS), ZS) → U1(N, XS, M, YS, ZS, sum_in(.(N, XS), .(s(M), YS), ZS))
U1(N, XS, M, YS, ZS, sum_out(.(N, XS), .(s(M), YS), ZS)) → sum_out(.(s(N), XS), .(M, YS), ZS)
U2(XS, YS, ZS, sum_out(XS, YS, ZS)) → sum_out(.(0, XS), YS, ZS)
U3(N, M, XS, X, sum_out(.(N, .(M, XS)), .(0, XS), YS)) → U4(N, M, XS, X, weight_in(YS, X))
U4(N, M, XS, X, weight_out(YS, X)) → weight_out(.(N, .(M, XS)), X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
SUM_IN(.(0, XS), YS, ZS) → SUM_IN(XS, YS, ZS)
SUM_IN(.(s(N), XS), .(M, YS), ZS) → SUM_IN(.(N, XS), .(s(M), YS), ZS)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ PiDP
SUM_IN(.(s(N), XS), .(M, YS)) → SUM_IN(.(N, XS), .(s(M), YS))
SUM_IN(.(0, XS), YS) → SUM_IN(XS, YS)
No rules are removed from R.
SUM_IN(.(0, XS), YS) → SUM_IN(XS, YS)
POL(.(x1, x2)) = 2·x1 + 2·x2
POL(0) = 0
POL(SUM_IN(x1, x2)) = 2·x1 + 2·x2
POL(s(x1)) = x1
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ PiDP
SUM_IN(.(s(N), XS), .(M, YS)) → SUM_IN(.(N, XS), .(s(M), YS))
SUM_IN(.(s(N), XS), .(M, YS)) → SUM_IN(.(N, XS), .(s(M), YS))
POL(.(x1, x2)) = 2·x1 + x2
POL(SUM_IN(x1, x2)) = 2·x1 + x2
POL(s(x1)) = 2 + x1
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ PisEmptyProof
↳ PiDP
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
U31(N, M, XS, X, sum_out(.(N, .(M, XS)), .(0, XS), YS)) → WEIGHT_IN(YS, X)
WEIGHT_IN(.(N, .(M, XS)), X) → U31(N, M, XS, X, sum_in(.(N, .(M, XS)), .(0, XS), YS))
weight_in(.(X, []), X) → weight_out(.(X, []), X)
weight_in(.(N, .(M, XS)), X) → U3(N, M, XS, X, sum_in(.(N, .(M, XS)), .(0, XS), YS))
sum_in([], YS, YS) → sum_out([], YS, YS)
sum_in(.(0, XS), YS, ZS) → U2(XS, YS, ZS, sum_in(XS, YS, ZS))
sum_in(.(s(N), XS), .(M, YS), ZS) → U1(N, XS, M, YS, ZS, sum_in(.(N, XS), .(s(M), YS), ZS))
U1(N, XS, M, YS, ZS, sum_out(.(N, XS), .(s(M), YS), ZS)) → sum_out(.(s(N), XS), .(M, YS), ZS)
U2(XS, YS, ZS, sum_out(XS, YS, ZS)) → sum_out(.(0, XS), YS, ZS)
U3(N, M, XS, X, sum_out(.(N, .(M, XS)), .(0, XS), YS)) → U4(N, M, XS, X, weight_in(YS, X))
U4(N, M, XS, X, weight_out(YS, X)) → weight_out(.(N, .(M, XS)), X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
U31(N, M, XS, X, sum_out(.(N, .(M, XS)), .(0, XS), YS)) → WEIGHT_IN(YS, X)
WEIGHT_IN(.(N, .(M, XS)), X) → U31(N, M, XS, X, sum_in(.(N, .(M, XS)), .(0, XS), YS))
sum_in(.(0, XS), YS, ZS) → U2(XS, YS, ZS, sum_in(XS, YS, ZS))
sum_in(.(s(N), XS), .(M, YS), ZS) → U1(N, XS, M, YS, ZS, sum_in(.(N, XS), .(s(M), YS), ZS))
U2(XS, YS, ZS, sum_out(XS, YS, ZS)) → sum_out(.(0, XS), YS, ZS)
U1(N, XS, M, YS, ZS, sum_out(.(N, XS), .(s(M), YS), ZS)) → sum_out(.(s(N), XS), .(M, YS), ZS)
sum_in([], YS, YS) → sum_out([], YS, YS)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
U31(sum_out(YS)) → WEIGHT_IN(YS)
WEIGHT_IN(.(N, .(M, XS))) → U31(sum_in(.(N, .(M, XS)), .(0, XS)))
sum_in(.(0, XS), YS) → U2(sum_in(XS, YS))
sum_in(.(s(N), XS), .(M, YS)) → U1(sum_in(.(N, XS), .(s(M), YS)))
U2(sum_out(ZS)) → sum_out(ZS)
U1(sum_out(ZS)) → sum_out(ZS)
sum_in([], YS) → sum_out(YS)
sum_in(x0, x1)
U2(x0)
U1(x0)
The following rules are removed from R:
U31(sum_out(YS)) → WEIGHT_IN(YS)
WEIGHT_IN(.(N, .(M, XS))) → U31(sum_in(.(N, .(M, XS)), .(0, XS)))
Used ordering: POLO with Polynomial interpretation [25]:
sum_in([], YS) → sum_out(YS)
POL(.(x1, x2)) = x1 + 2·x2
POL(0) = 0
POL(U1(x1)) = x1
POL(U2(x1)) = x1
POL(U31(x1)) = x1
POL(WEIGHT_IN(x1)) = 1 + 2·x1
POL([]) = 2
POL(s(x1)) = x1
POL(sum_in(x1, x2)) = x1 + 2·x2
POL(sum_out(x1)) = 2 + 2·x1
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof
sum_in(.(0, XS), YS) → U2(sum_in(XS, YS))
sum_in(.(s(N), XS), .(M, YS)) → U1(sum_in(.(N, XS), .(s(M), YS)))
U1(sum_out(ZS)) → sum_out(ZS)
U2(sum_out(ZS)) → sum_out(ZS)
sum_in(x0, x1)
U2(x0)
U1(x0)